A:Type, eq:EqDecider(A), f, g:a:A fp Top, x:A. x  dom(f  g) ~ (x  dom(f)  x  dom(g)) 

latex

Definitions	t  T, x:A. B(x), b, {T}, P  Q, Top, P  Q, P  Q, x. t(x), P & Q, P  Q, f  g, false, , true, A, b, Prop, Unit, EqDecider(T), a:A fp B(a), p  q, SQType(T), x  dom(f), False
Lemmas	not functionality wrt iff, bool sq, fpf wf, deq wf, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool wf, eqtt to assert, fpf-join wf, fpf-join-dom, top wf, assert wf, fpf-dom wf